judgmental equality

judgmental equality

f(x) :≡ λx.x + y があったときに、()の中の束縛変数をyにしてf(y)にすると

f(y) :≡ λy.y + yになって捕捉される自由変数の補足問題がある。

こういうときにバッティングしないようにzにしてλz.x + zのようにする。

λy. x + yとλz. x + zの関係、f(y)とλz. y + zの関係は以下のように表現される。

λy. x + y is judgmentally equal to λz. x + z.

f(y) judgmentally equal to λz. y + z

De Bruijn インデックスによる解決方法による解決方法もある。

確認用

Q. judgmental equality

参考